perm filename REM[ESS,JMC] blob
sn#016781 filedate 1972-12-08 generic text, type T, neo UTF8
(ADDAXIOM TRI
((FORALL X) ((FORALL Y) (OR (LESSP X Y) (LESSP Y X) (EQUAL X Y)))))
(ADDAXIOM TRI1
((FORALL X) ((FORALL Y) (NOT (AND (LESSP X Y) (LESSP Y X))))))
(ADDAXIOM TRI2
((FORALL X) ((FORALL Y) (NOT (AND (EQUAL X Y) (LESSP Y X))))))
(ADDAXIOM TRI3
((FORALL X) ((FORALL Y) (NOT (AND (EQUAL X Y) (LESSP X Y))))))
(ADDAXIOM EVOD ((FORALL X) (EQUIVALENT (EVEN X) (NOT (ODD X)))))
(ADDAXIOM EXOY
((FORALL X) (IMPLIES (AND (EVEN X) (ODD Y)) (NOT (EQUAL X Y)))))
(GIVEPROOF ONE
((1 (OR (LESSP A B) (LESSP B A) (EQUAL A B)) (USEAX TRI A B) NIL)
(2 (OR (LESSP B A) (LESSP A B) (EQUAL B A)) (USEAX TRI B A) NIL)
(3 (NOT (AND (LESSP A B) (LESSP B A))) (USEAX TRI1 A B) NIL)
(4 (NOT (AND (LESSP B A) (LESSP A B))) (USEAX TRI1 B A) NIL)
(5 (NOT (AND (EQUAL B A) (LESSP A B))) (USEAX TRI2 B A) NIL)
(6 (NOT (AND (EQUAL A B) (LESSP B A))) (USEAX TRI2 A B) NIL)
(7 (NOT (AND (EQUAL A B) (LESSP A B))) (USEAX TRI3 A B) NIL)
(8 (NOT (AND (EQUAL B A) (LESSP B A))) (USEAX TRI3 B A) NIL)
(9 (EQUIVALENT (EVEN A) (NOT (ODD A))) (USEAX EVOD A) NIL)
(10 (EQUIVALENT (EVEN B) (NOT (ODD B))) (USEAX EVOD B) NIL)
(11 (IMPLIES (AND (EVEN B) (ODD Y)) (NOT (EQUAL B Y)))
(USEAX EXOY B)
NIL)
(12 (IMPLIES (AND (EVEN A) (ODD Y)) (NOT (EQUAL A Y)))
(USEAX EXOY A)
NIL)))